(declare-sort S0 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Bool)) (not (or q2 v4 v7 q2 q0))))
(declare-const v11 Bool)
(assert (=> v1 (not v10)))
(declare-const v12 Bool)
(assert (=> v1 (not v10)))
(declare-const v13 Bool)
(assert (forall ((q3 (_ BitVec 11)) (q4 (_ BitVec 110)) (q5 Bool)) (and (xor v11 q5 q5 q5 q5 v13) (= q3 #b01101111111) (bvuge ((_ repeat 10) #b01101111111) ((_ repeat 10) #b01101111111)))))
(declare-const v14 Bool)
(assert v0)
(assert (xor v5 v3 v13 v8 v6 v5 v4 v2 v13 v5 v3))
(declare-const S0-0 S0)
(declare-const v15 Bool)
(assert v2)
(assert v13)
(assert v8)
(assert (forall ((q6 (_ BitVec 11)) (q7 (_ BitVec 110)) (q8 (_ BitVec 110))) (=> (= (bvnor ((_ repeat 10) #b01101111111) ((_ repeat 10) #b01101111111)) q7 q8 q8 q8) (distinct q6 #b01101111111 #b01101111111 #b01101111111 q6))))
(assert (=> v8 v6))
(check-sat)
